deferred val +' : (int * int) -> int
where (forall (x, y). pre ( +') (x, y))
  and (forall (x, y, z). post ( +' ) (x, y) (z) <=> z = x + y)

let f (x) returns y where (y = x + 3) = 
  let y = x +' 2 in
  let y = y +' 1 in
     y
